Termination w.r.t. Q proof of /tmp/tmptx5MP1/quotminus.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MIN(min(X, Y), Z) → PLUS(Y, Z)
QUOT(s(X), s(Y)) → QUOT(min(X, Y), s(Y))
MIN(s(X), s(Y)) → MIN(X, Y)
QUOT(s(X), s(Y)) → MIN(X, Y)
MIN(min(X, Y), Z) → MIN(X, plus(Y, Z))
PLUS(s(X), Y) → PLUS(X, Y)

The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MIN(min(X, Y), Z) → PLUS(Y, Z)
QUOT(s(X), s(Y)) → QUOT(min(X, Y), s(Y))
MIN(s(X), s(Y)) → MIN(X, Y)
QUOT(s(X), s(Y)) → MIN(X, Y)
MIN(min(X, Y), Z) → MIN(X, plus(Y, Z))
PLUS(s(X), Y) → PLUS(X, Y)

The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 2 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PLUS(s(X), Y) → PLUS(X, Y)

The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

PLUS(s(X), Y) → PLUS(X, Y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(PLUS(x₁, x₂)) = (2)x_1
POL(s(x₁)) = 1/4 + (7/2)x_1

The value of delta used in the strict ordering is 1/2.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MIN(s(X), s(Y)) → MIN(X, Y)
MIN(min(X, Y), Z) → MIN(X, plus(Y, Z))

The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MIN(s(X), s(Y)) → MIN(X, Y)
MIN(min(X, Y), Z) → MIN(X, plus(Y, Z))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(plus(x₁, x₂)) = 2 + (7/2)x_1 + (4)x_2
POL(MIN(x₁, x₂)) = (4)x_1
POL(s(x₁)) = 4 + (2)x_1
POL(Z) = 1/4
POL(min(x₁, x₂)) = 4 + (11/4)x_1 + (4)x_2
POL(0) = 0

The value of delta used in the strict ordering is 16.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

QUOT(s(X), s(Y)) → QUOT(min(X, Y), s(Y))

The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

QUOT(s(X), s(Y)) → QUOT(min(X, Y), s(Y))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(plus(x₁, x₂)) = 0
POL(QUOT(x₁, x₂)) = (9/4)x_1
POL(s(x₁)) = 4 + (15/4)x_1
POL(Z) = 0
POL(min(x₁, x₂)) = 11/4 + (3/2)x_1
POL(0) = 0

The value of delta used in the strict ordering is 45/16.
The following usable rules [17] were oriented:

min(X, 0) → X
min(min(X, Y), Z) → min(X, plus(Y, Z))
min(s(X), s(Y)) → min(X, Y)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
min(X, 0) → X
min(s(X), s(Y)) → min(X, Y)
min(min(X, Y), Z) → min(X, plus(Y, Z))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.